<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>CAmkES Internals | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/projects/">
              <span property="name"><b>Projects</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/projects/camkes/">
              <span property="name"><b>CAmkES</b></span>
            </a>
            <meta property="position" content="3" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">CAmkES Internals</span>
            <meta property="position" content="4" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    


<div class="sidebar">















    <ul class="nav nav-sidebar">
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4/">seL4</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/l4v/">L4.verified</a>
        </li>
  
    
    

    
        <li class="active">
            <a class="" href="/projects/camkes/">CAmkES</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/capdl/">CapDL</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/elfloader/">Elfloader</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/buildsystem/">seL4 Buildsystem</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/user_libs/">user_libs</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4runtime/">The seL4 run-time</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4webserver/">seL4webserver</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4-tutorials/">seL4 tutorials</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4bench/">sel4bench</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4test/">seL4Test</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/virtualization/">Virtualization</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/camkes-vm/">camkes-vm</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/dockerfiles/">Dockerfiles</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/docsite/">seL4 Documentation website</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/sel4_tools/">seL4_tools</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/microkit/">Microkit</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/hardware_hacks/">Hardware Hacks</a>
        </li>
  
    
    

    
        <li class="">
            <a class="" href="/projects/rust/">Rust</a>
        </li>
  
    </ul>


</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">
    <h1 id="camkes-internals">CAmkES Internals</h1>

<h2 id="overview">Overview</h2>

<p>From the top, the CAmkES tool (typically found in “tools/camkes/camkes.sh”) is a program that generates a <strong>single</strong> file that makes up part of the source of a seL4 application. There are a variety of types of files it can generate:</p>

<ul>
  <li>a capdl spec describing the cap distribution of the entire
      CAmkES spec</li>
  <li>a C file containing generated glue code for a component or
      connector</li>
  <li>a Makefile that knows how to invoke the CAmkES tool to generate
      all the files required to compile the application (besides the
      Makefile itself)</li>
</ul>

<p>A typical build of a CAmkES application looks like:</p>

<ol>
  <li>
    <p>Generate makefile (this file will be called “camkes-gen.mk”)</p>
  </li>
  <li>
    <p>Invoke generated makefile</p>

    <ol>
      <li>Copy sources into build directory</li>
      <li>Generated glue code for components and connectors</li>
      <li>Compile each component</li>
      <li>Run CapDL filters</li>
      <li>Generate CapDL spec</li>
      <li>Compile CapDL loader</li>
    </ol>
  </li>
</ol>

<h2 id="caching">Caching</h2>

<p>Remember that the CAmkES tool only generates one file each time it’s
run, and in a single build it’s typically run many times. This means,
all the input files must be parsed again for each output file. The CapDL
database is built up by logic in the templates that generate glue code,
which means that when the capdl spec is generated, all the templates
must be re-instantiated to get the spec into the right state. This all
seems to unnecessarily repeat a lot of work.</p>

<p>To get around this, CAmkES contains several caches:</p>

<h3 id="camkes-accelerator">CAmkES Accelerator</h3>

<p>Output files are cached with keys computed from hashes of the CAmkES
spec. This prevents re-generating most files during a single build of a
CAmkES app.</p>

<h3 id="data-structure-cache">Data Structure Cache</h3>

<p>This stores the AST and CapDL database persistently (using pickle)
across each invocation of the CAmkES tool in a single build of a CAmkES
app. This removes the need to parse the CAmkES spec multiple times in a
single build, and also removes the need to re-instantiate component and
connector templates to re-build the CapDL database.</p>

<h2 id="creating-component-address-spaces">Creating Component Address Spaces</h2>

<p>CAmkES creates a CapDL spec representing the entire application (ie. all
components and connections). Part of the spec is the hierarchy of paging
objects comprising the address space of each component. This is actually
done by the python CapDL library. After each component is compiled, but
before the CapDL Filters (see below) are applied,
<a href="https://github.com/seL4/camkes-tool/blob/master/camkes/runner/__main__.py">the python capdl library is invoked (search for get_spec)</a> to inspect
the ELF file produced by compiling the component and create all the
paging structures it needs.</p>

<h3 id="collapse-shared-frames">Collapse Shared Frames</h3>

<p>Dataport connections in CAmkES establish a region of shared memory
between components. When a pair of components share memory, there must
be common frames mapped into both of their address spaces. When each
component gets compiled, any dataports are just treated as an
appropriately sized buffer. We need a way to inform the system
initializer (the CapDL Loader) that when setting up these components’
address spaces, to make the vaddr of the symbol associated with the
dataport in each component map to the same physical memory. During
template instantiation, a database of shared memory regions is
populated. The dataport templates all update this database with the
regions of shared memory they require. The “Collapse Shared Frames”
filter queries this database to find all the regions of shared memory,
then updates the CapDL database, changing memory mappings in the address
space of one component, so it points to the frames already mapped into
the address space of the other component. The frames in the first
component are then removed from the spec.</p>

<h3 id="remove-tcb-caps">Remove TCB Caps</h3>

<p>CAmkES has the option to prevent components from being given a cap to
their own TCB. This is implemented as a CapDL Filter, which examines the
cspace (CNode hierarchy) of each component (really each TCB, as
components may have several threads), and removes any caps to any TCBs
that are part of that component.</p>

<h3 id="guard-pages">Guard Pages</h3>

<p>This filter adds guard pages around the stacks of all threads. For each
thread in the system, the ELF that contains the program that will run on
that thread contains a symbol identifying the stack for that thread.
This filter looks up the vaddr and size of that symbol in the ELF, and
modifies the CapDL spec to make sure there’s no frame mapped in
immediately before or after the stack.</p>

<h2 id="template-context">Template Context</h2>

<p>The python-looking functions called from within templates (e.g.
<code class="language-plaintext highlighter-rouge">alloc_cap</code>, <code class="language-plaintext highlighter-rouge">register_shared_variable</code>) are actually keys in a dict
defined here:
<a href="https://github.com/seL4/camkes-tool/blob/master/camkes/runner/Context.py">https://github.com/seL4/camkes-tool/blob/master/camkes/runner/Context.py</a>.
There are even some values (such as <code class="language-plaintext highlighter-rouge">seL4_EndpointObject</code>), modules (such
as <code class="language-plaintext highlighter-rouge">sys</code>), and seemingly built-in functions (e.g. <code class="language-plaintext highlighter-rouge">zip</code>) passed through
using this dict. You can update this dict to add new functions to the
template context. Some of these functions are called “in the context” of
the template they are instantiating. That is, for component and
connector templates, the generated code will be part of a single
component (each connector has a separate template for each side of the
connection). The most common example of this is when allocating a cap,
the cnode/cspace that will contain the cap isn’t passed to <code class="language-plaintext highlighter-rouge">alloc_cap</code> in
the template code, but rather implied by the component for which the
template is being instantiated.</p>

<h3 id="object-space-and-cap-space">Object Space and Cap Space</h3>

<p>A template context is created with an “object space” and “cap space”.
These are terms from the python CapDL library. An object space tracks
all the objects that will exist in the system the CapDL spec describes.
There is a single object space for an entire CAmkES application. A cap
space tracks all the caps that will be placed in a particular cspace.
There is one cap space for each component. When calling <code class="language-plaintext highlighter-rouge">alloc_cap</code> in a
template on behalf of a component, the cap is placed in that component’s
cap space. The resulting CapDL spec will include in one of that
component’s CNodes, an entry for the allocated cap.</p>

<h3 id="template-functions">Template Functions</h3>

<p>Here are some of the complicated functions in the template context:</p>

<h4 id="alloc_objname-type">alloc_obj(name, type)</h4>

<p>Updates the CapDL database to contain a new object with a given name and
type, returning a (python) reference to that object. Doesn’t create any
caps.</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>/*- set ep = alloc_obj("my_ep", seL4_EndpointObject) -*/
</code></pre></div></div>

<h4 id="alloc_capname-object">alloc_cap(name, object)</h4>

<p>Updates the CapDL database, adding a named cap to a given object to the
current component’s cap space, returning the CPtr of the cap.</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>// continues from above
/*- set ep_cap = alloc_cap("my_ep_cap", ep) -*/
seL4_Wait(/*? ep_cap ?*/);
</code></pre></div></div>

<h4 id="allocname-type">alloc(name, type)</h4>

<p>Effectively equivalent <code class="language-plaintext highlighter-rouge">to alloc_cap(name, alloc_obj(name, type))</code></p>

<h2 id="simple">Simple</h2>

<p>Simple is an interface in the seL4 libraries for accessing information
about your environment, typically about which capabilities are
available. CAmkES has an implementation of simple which a component can
use to access (some of) its caps. It’s implemented as a jinja template:
<a href="https://github.com/seL4/camkes-tool/blob/master/camkes/templates/component.simple.c">https://github.com/seL4/camkes-tool/blob/master/camkes/templates/component.simple.c</a></p>

<p>A component instance can be built with this simple implementation by
adding the following to the assembly:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>configuration {
   instance_name.simple = true;
}
</code></pre></div></div>

<h2 id="template-instantiation-order">Template Instantiation Order</h2>

<p>CAmkES instantiates templates in the following order: makefile,
components, connections, simple, capdl. The makefile has to come first
since it defines the build rules that instantiate all the other
templates. Simple must come after components and connections as it needs
to generate code to give access to caps allocated in component and
connection templates. Capdl must be last as it needs to be run after
compiling all components (including code generated by the simple
template). Since each template may be instantiated while producing any
output file, in order for caching to work correctly, the order of
template instantiation must be deterministic, at least in a single
invocation of the CAmKES-tool.</p>

<p>Note that components and connections will be instantiated in arbitrary
(but deterministic) order. An implication of this, is that if multiple
components want a cap to the same object (e.g. an endpoint which two
components use to communicate), each template that needs to talk about a
cap to the object must first allocate it unless it’s already allocated.
This is because you can’t talk about a cap to an object until that
object has been allocated. Typically in such a situation, you’ll see the
following template code on both sides of the connection:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>/*- set ep = alloc_obj('ep_obj_name', seL4_EndpointObject) -*/
/*- set ep_cap = alloc_cap('this_components_ep_cap', ep) -*/

// do something with ep_cap
</code></pre></div></div>

<p>Looking at the code, it appears the endpoint will be allocated twice, as
both sides of the connection will call <code class="language-plaintext highlighter-rouge">alloc_obj</code>. Digging deeper into
the implementation of <code class="language-plaintext highlighter-rouge">alloc_obj</code>, we see it calls a function called
<code class="language-plaintext highlighter-rouge">guard</code>. <code class="language-plaintext highlighter-rouge">guard</code> is a bit of a misnomer. A more appropriate name might be
<code class="language-plaintext highlighter-rouge">allocate_unless_already_allocated</code>. It checks whether there’s already
an object by the given name, returns the object if it exists, otherwise
allocates and returns it.</p>

  </div>







  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#overview">Overview</a></li>
<li class="toc-entry toc-h2"><a href="#caching">Caching</a>
<ul>
<li class="toc-entry toc-h3"><a href="#camkes-accelerator">CAmkES Accelerator</a></li>
<li class="toc-entry toc-h3"><a href="#data-structure-cache">Data Structure Cache</a></li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#creating-component-address-spaces">Creating Component Address Spaces</a>
<ul>
<li class="toc-entry toc-h3"><a href="#collapse-shared-frames">Collapse Shared Frames</a></li>
<li class="toc-entry toc-h3"><a href="#remove-tcb-caps">Remove TCB Caps</a></li>
<li class="toc-entry toc-h3"><a href="#guard-pages">Guard Pages</a></li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#template-context">Template Context</a>
<ul>
<li class="toc-entry toc-h3"><a href="#object-space-and-cap-space">Object Space and Cap Space</a></li>
<li class="toc-entry toc-h3"><a href="#template-functions">Template Functions</a>
<ul>
<li class="toc-entry toc-h4"><a href="#alloc_objname-type">alloc_obj(name, type)</a></li>
<li class="toc-entry toc-h4"><a href="#alloc_capname-object">alloc_cap(name, object)</a></li>
<li class="toc-entry toc-h4"><a href="#allocname-type">alloc(name, type)</a></li>
</ul>
</li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#simple">Simple</a></li>
<li class="toc-entry toc-h2"><a href="#template-instantiation-order">Template Instantiation Order</a></li>
</ul>
</div>

  
  
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
  
    <ul class="section-nav">
    	<h2> CAmkES </h2> 
        <li>
          
          <a style="" class="" href="/projects/camkes/">
            Documentation homepage
          </a>
        </li>


        <li>
          
          <a style="" class="" href="/projects/camkes/status.html">
            Status
          </a>
        </li>












    
        <h3>Useful URLs</h3>
    
        <li>
          <a style="" class="" href="/projects/camkes/manual.html">
            CAmkES Manual
          </a>
        </li>

    
        <li>
          <a style="" class="" href="https://trustworthy.systems/projects/TS/camkes.pml">
            Trustworthy Systems CAmkES project
          </a>
        </li>





    
        <h3>Repositories</h3>
    
        <li>
          <a class="" href="https://github.com/sel4/camkes-tool">
            camkes-tool
          </a>
        </li>

    
        <li>
          <a class="" href="https://github.com/sel4/camkes">
            camkes
          </a>
        </li>

    
        <li>
          <a class="" href="https://github.com/sel4/camkes-manifest">
            camkes-manifest
          </a>
        </li>

    
        <li>
          <a class="" href="https://github.com/sel4proj/global-components">
            global-components
          </a>
        </li>









  
      
          <h3>Releases</h3>
      
          <li>
            <a style="" href="/releases/camkes/camkes-3.9.0.html">
              camkes-3.9.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-3.8.0.html">
              camkes-3.8.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-3.7.0.html">
              camkes-3.7.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-3.6.0.html">
              camkes-3.6.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-3.5.0.html">
              camkes-3.5.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-3.4.0.html">
              camkes-3.4.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-3.3.0.html">
              camkes-3.3.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-3.2.0.html">
              camkes-3.2.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-3.11.0.html">
              camkes-3.11.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-3.10.0.html">
              camkes-3.10.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-3.1.0.html">
              camkes-3.1.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-3.0.0.html">
              camkes-3.0.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-2.3.1.html">
              camkes-2.3.1
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-2.3.0.html">
              camkes-2.3.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-2.2.0.html">
              camkes-2.2.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-2.1.0.html">
              camkes-2.1.0
            </a>
          </li>
  
      
          <li>
            <a style="" href="/releases/camkes/camkes-2.0.0.html">
              camkes-2.0.0
            </a>
          </li>
  







    </ul>

</div>


</div>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Tue Mar 9 13:04:54 2021 +1100 6eb8c7ffa9
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/projects/camkes/internals.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/projects/camkes/internals.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
